FDL - Nuprl Definition : existse-rcv

Nuprl Definition : existse-rcv

0,22

e=rcv(l,tg). P(e) ==

e:E. kind(e) = rcv(l,tg) & P(e)

clarification:

existse-rcv(es;l;tg;e.P(e)) ==

e:es-E(es). es-kind(es; e) = rcv(l,tg)

Knd & P(e)

Definitions x:A. B(x), E, P & Q, Knd, kind(e), rcv(l,tg)

FDL editor aliases existse-rcv

Definitions	x:A. B(x), E, P & Q, Knd, kind(e), rcv(l,tg)
FDL editor aliases	existse-rcv